EN FR
EN FR




Section: Contracts and Grants with Industry

Grants with Industry

FNRAE projects

Ascert

  • Title: Analyses Statiques CERTifiés

  • Type: 6th call: Verification methods for software and systems

  • Instrument: FNRAE grant

  • Duration: April 2009 - March 2012

  • Coordinator: INRIA (France)

  • Others partners: INRIA-Bretagne Atlantique, the INRIA Rhône-Alpes, the INRIA Paris-Rocquencourt, and the ENS.

  • See also: http://ascert.gforge.inria.fr/

  • Abstract: Although static analyzers have demonstrated their ability to prove the absence of large classes of errors in critical software, they are themselves large and complex software, so it is natural to question their implementation correctness and the validity of their output. The focus of the Ascert project is the use of formal methods to ensure the correctness of an analyzer with respect to the abstraction interpretation theory. Methods to be investigated include the direct proof of the analyzer, the proof of a verifier for the analyzer result, and the validation of the inductive invariants generated by the analyzer, using the Coq proof assistant. These methods will be applied to the certification of several numerical abstract domains, of an abstract interpreter for imperative programs and its possible extensions to one of the formal semantics of the CompCert verified C compiler.

Sardanes

  • Title: Sémantique, Analyse et tRansformation Des Applications Numériques Embarqués Synchrones

  • Type: 6th call: Verification methods for software and systems

  • Instrument: FNRAE grant

  • Duration: February 2009 - September 2013

  • Coordinator: Université de Perpignan

  • Others partners: Université de Perpignan and the ENS.

  • See also: http://perso.univ-perp.fr/mmartel/sardanes.html

  • Abstract: Scade is widely used to write critical embedded software, as a specification and verification language. The semantics of Scade uses real arithmetics whereas it is compiled into a language that uses floating-point arithmetics. The goal of the Sardanes project is to use expression transformation so as to ensure that the numerical properties of the programs is preserved during the compilation. Patrick Cousot and Radhia Cousot are the principal investigators for this action.